module SAU

where 

import List

type Name     = String
type Index    = [Int]
data Id       = Id Name Index deriving (Eq,Ord)

instance Show Id where 
  show (Id name [])  = name
  show (Id name [i]) = name ++ ('_': show i)
  show (Id name is)  = name ++ ('_': showInts is)
     where showInts [] = ""  
           showInts (i:is) = show i ++ showInts is

ix = Id "x" []
iy = Id "y" []
iz = Id "z" []

data Term     = Var Id | Struct Id [Term] deriving Eq

instance Ord Term where 
  compare (Var x) (Var y) = compare x y 
  compare (Var x) _       = LT
  compare _       (Var y) = GT 
  compare (Struct a ts) (Struct b rs) | a == b = compare ts rs
                                      | a < b  = LT
                                      | a > b  = GT

x    = Var ix
y    = Var iy
z    = Var iz

a     = Struct (Id "a" []) []
b     = Struct (Id "b" []) []
c     = Struct (Id "c" []) []
zero  = Struct (Id "z" []) []
s     = Struct (Id "s" [])
t     = Struct (Id "t" [])
u     = Struct (Id "u" [])
one   = s[zero]
two   = s[one]
three = s[two]
four  = s[three]
five  = s[four]

instance Show Term where 
  show (Var id)         = show id 
  show (Struct id [])   = show id 
  show (Struct id ts)   = show id ++ concat [ show ts ]

isVar :: Term -> Bool
isVar (Var _) = True
isVar _       = False

varsInTerm :: Term -> [Id]
varsInTerm (Var i)       = [i]
varsInTerm (Struct i ts) = varsInTerms ts

varsInTerms :: [Term] -> [Id]
varsInTerms = nub . concat . map varsInTerm

data Form =  Atom Id [Term]
           | Eq Term Term
           | Neg Form
           | Impl Form Form
           | Equi Form Form 
           | Conj [Form]
           | Disj [Form] 
           | Forall Id Form 
           | Exists Id Form
     deriving (Eq,Ord)

instance Show Form where 
  show (Atom id []) = show id 
  show (Atom id ts) = show id ++ concat [ show ts ]
  show (Eq t1 t2)   = show t1 ++ "==" ++ show t2
  show (Neg form)   = '~': (show form)
  show (Impl f1 f2) = "(" ++ show f1 ++ "==>" ++ show f2 ++ ")"
  show (Equi f1 f2) = "(" ++ show f1 ++ "<=>" ++ show f2 ++ ")"
  show (Conj []) =  "true" 
  show (Conj fs) =  "conj" ++ concat [ show fs ]
  show (Disj []) =  "false" 
  show (Disj fs) =  "disj" ++ concat [ show fs ]
  show (Forall id f) = "A" ++  show id ++ (' ' : show f)
  show (Exists id f) = "E" ++  show id ++ (' ' : show f)

type Subst = [(Id,Term)]

epsilon :: Subst
epsilon = []

dom :: Subst -> [Id]
dom = map fst

rng :: Subst -> [Term]
rng = map snd 

restriction :: [Id] -> Subst -> Subst
restriction ids = filter (\ (x,_) -> elem x ids)

appI :: Subst -> Id -> Term
appI []          y             = (Var y)
appI ((x,x'):xs) y | x == y    = x'
                   | otherwise = appI xs y 

appT :: Subst -> Term -> Term
appT b (Var y)       = appI b y
appT b (Struct n ts) = Struct n (appTs b ts) 

appTs :: Subst -> [Term] -> [Term]
appTs = map . appT

appF :: Subst -> Form -> Form 
appF b (Atom a ts)        = Atom a (appTs b ts)
appF b (Neg form)         = Neg (appF b form)
appF b (Impl form1 form2) = Impl (appF b form1) (appF b form2) 
appF b (Equi form1 form2) = Equi (appF b form1) (appF b form2) 
appF b (Conj forms)       = Conj (appFs b forms)
appF b (Disj forms)       = Disj (appFs b forms)
appF b (Forall v form)    = Forall v (appF b' form) 
                            where b' = filter (\ (x,x') -> x /= v) b
appF b (Exists v form)    = Exists v (appF b' form) 
                            where b' = filter (\ (x,x') -> x /= v) b

appFs :: Subst -> [Form] -> [Form]
appFs b = map (appF b)

cleanUp :: Subst -> Subst
cleanUp = filter (\ (x,x') -> x' /= (Var x))

compose :: Subst -> Subst -> Subst 
compose xs ys = 
  (cleanUp [ (y,(appT xs y')) | (y,y') <-  ys ])
   ++
  (filter (\ (x,x') -> x `notElem` (dom ys)) xs)

demo1 = compose [(ix,y)] [(iy,x)]
demo2 = compose [(iy,x)] [(ix,y)]
demo3 = compose [(iy,z)] [(ix,y)]

isRenaming :: Subst -> Bool
isRenaming sigma = all isVar rngSigma && (nub rngSigma) == rngSigma
  where rngSigma = rng sigma

unifyTs :: Term -> Term -> [Subst]
unifyTs (Var x)       (Var y)       =
        if x==y then [epsilon] else [[(x,Var y)]]
unifyTs (Var x)       t2            = 
        [ [(x,t2)] | x `notElem` varsInTerm t2 ]
unifyTs t1            (Var y)       = 
        [ [(y,t1)] | y `notElem` varsInTerm t1 ]
unifyTs (Struct a ts) (Struct b rs) = 
        [ u | a==b, u <- unifyTlists ts rs ]

unifyTlists :: [Term] -> [Term] -> [Subst]
unifyTlists []     []     = [epsilon]
unifyTlists []     (r:rs) = []
unifyTlists (t:ts) []     = []
unifyTlists (t:ts) (r:rs) = 
   [ (compose sigma2 sigma1) | sigma1 <- unifyTs t r,
                               sigma2 <- unifyTlists (appTs sigma1 ts) 
                                                     (appTs sigma1 rs) ]

unif :: Term -> Term -> Subst
unif tm1 tm2 = case unifyTs tm1 tm2 of 
   []  -> error "terms do not unify"
   [s] -> s

skolem ::  Int -> [Id] -> Term
skolem k is = Struct (Id "sk" [k]) [ (Var x) | x <- is ]

sk :: Form -> Form
sk f = fst (skf f [] True 0) 

skf :: Form -> [Id] -> Bool -> Int -> (Form,Int)
skf (Atom n ts) ixs pol k = ((Atom n ts),k)
skf (Conj fs) ixs pol k = ((Conj fs'),j) 
      where (fs',j) = skfs fs ixs pol k 
skf (Disj fs) ixs pol k = ((Disj fs'),j) 
      where (fs',j) = skfs fs ixs pol k 
skf (Forall x f) ixs True k = ((Forall x f'),j) 
     where (f',j) = skf f ixs' True k 
           ixs'   = insert x ixs
skf (Forall x f) ixs False k = skf (appF b f) ixs False (k+1)
     where b = [(x,(skolem k ixs))]
skf (Exists x f) ixs True k = skf (appF b f) ixs True (k+1) 
     where b = [(x,(skolem k ixs))]
skf (Exists x f) ixs False k = ((Exists x f'),j) 
     where (f',j) = skf f ixs' False k 
           ixs'   = insert x ixs
skf (Neg f) ixs pol k = ((Neg f'),j)
     where (f',j) = skf f ixs (not pol) k 

skfs :: [Form] -> [Id] -> Bool -> Int -> ([Form],Int)
skfs []     _   _   k  = ([],k)
skfs (f:fs) ixs pol k  = ((f':fs'),j) 
   where 
   (f', j1) = skf  f  ixs pol k
   (fs',j)  = skfs fs ixs pol j1 

p      = Atom (Id "p" [])
q      = Atom (Id "q" [])
r      = Atom (Id "r" [])

refl   = Forall ix (r [x,x])
irrefl = Forall ix (Neg (r [x,x]))
trans  = Forall ix (Forall iy (Forall iz 
         (Disj [Neg (r [x,y]),Neg (r [y,z]),r [x,z]])))
ctrans = Forall ix (Forall iy (Forall iz 
         (Disj [r [x,y], r [y,z],Neg (r [x,z])])))
symm   = Forall ix (Forall iy 
         (Disj [Neg  (r [x,y]), r [y,x]]))
asymm  = Forall ix (Forall iy 
         (Disj [Neg  (r [x,y]), Neg (r [y,x])]))
serial = Forall ix (Exists iy (r [x,y]))
serial1 = Forall ix (Forall iy (Exists iz (r [x,y,z])))
serial2 = Forall ix (Exists iy (Exists iz (r [x,y,z])))
relprop1 = Disj [(Neg asymm),irrefl]
relprop2 = Disj [(Neg trans),(Neg irrefl),asymm]
relprop3 = Disj [(Neg trans),(Neg symm),(Neg serial),refl]

data Cl = Cl [Term] [Term] deriving (Eq,Ord,Show)

appCl :: Subst -> Cl -> Cl 
appCl sigma (Cl neg pos) = Cl (appTs sigma neg) (appTs sigma pos)

appCls :: Subst -> [Cl] -> [Cl]
appCls b = map (appCl b)

varsInClause :: Cl -> [Id]
varsInClause (Cl neg pos) = nub (varsInTerms neg ++ varsInTerms pos)

fuseLists :: Ord a => [a] -> [a] -> [a]
fuseLists [] ys = ys
fuseLists xs [] = xs
fuseLists (x:xs) (y:ys) | x < y  = x:(fuseLists xs (y:ys))
                        | x == y = x:(fuseLists xs ys) 
                        | x > y  = y:(fuseLists (x:xs) ys)

disjList :: [Cl] -> [Cl]
disjList []   = [Cl [] []]
disjList [cl] = [cl]
disjList (cl:cls) = map (disj cl) (disjList cls)
  where 
  disj (Cl neg pos) (Cl neg' pos') = 
        Cl (fuseLists neg neg') (fuseLists pos pos') 

cf :: Form -> [Cl]
cf (Atom n ts) = [Cl [] [Struct n ts]]
cf (Conj fs) = concat (map cf fs) 
cf (Disj fs) = disjList (concat (map cf fs))
cf (Neg (Atom n ts)) =  [Cl [Struct n ts] []]
cf (Neg (Conj fs)) = disjList (concat (map (\ f -> cf (Neg f)) fs))
cf (Neg (Disj fs)) = concat (map (\ f -> cf (Neg f)) fs)
cf (Neg (Neg f)) = cf f 

clause :: Form -> [Cl] 
clause = cf . sk

infix  6 :-
data Dclause =  Term :- [Term] deriving Show

type Goal   =  [Term]

father, fatherOf ::  [Term] -> Term
father = Struct (Id "father" [])
fatherOf = Struct (Id "father_of" [])

fatherC :: Dclause
fatherC = father [Var (Id "X" [])] 
          :- [fatherOf [Var (Id "X" []),Var (Id "_" [])]]

nil :: Term
nil  = Struct (Id "nil" []) [] 

cons :: [Term] -> Term
cons = Struct (Id "cons" [])

type Definition = (Name,[Dclause]) 
data Database   = Db [Definition] deriving Show

dclausesFor           :: Name -> Database -> [Dclause]
dclausesFor a (Db defs) = case dropWhile (\ (n,def) -> n<a) defs of
                          []          -> []
                          ((n,def):_) -> if a==n then def else []

renameVars                  :: Int -> Term -> Term
renameVars level (Var (Id s n))   = Var (Id s [level])
renameVars level (Struct s ts) = Struct s (map (renameVars level) ts)

renDclauses                  :: Database -> Int -> Term -> [Dclause]
renDclauses db n (Var _)          = []
renDclauses db n (Struct (Id a _) _) = 
             [r tm:-map r tp | (tm:-tp) <- dclausesFor a db]
                                where r = renameVars n

type Alt   = ([Term], Subst) 

alts       :: Database -> Int -> Term -> [Alt]
alts db n g = [ (tp,u) | (tm:-tp) <- renDclauses db n g, 
                          u       <- unifyTs g tm         ]

memb :: [Term] -> Term
memb = Struct (Id "member" []) 

member :: Definition 
member = ("member", [memb [x,cons [x,y]] :- [],
                     memb [x,cons [y,z]] :- [memb [x,z]]])

db = Db [member]

goal = memb [x, cons [a, cons [b, cons [c,nil]]]]

resolStep = alts db 0 goal

type Stack = [ (Subst, [Term], [Alt]) ]

prove :: Database -> [Term] -> [Subst]
prove db gl = solve 1 epsilon gl []
  where 
  solve :: Int -> Subst -> [Term] -> Stack -> [Subst]
  solve n s []     ow = s : backtrack n ow
  solve n s (g:gs) ow = choose n s gs (alts db n (appT s g)) ow

  choose :: Int -> Subst -> [Term] -> [Alt] -> Stack -> [Subst]
  choose n s gs []          ow = backtrack n ow
  choose n s gs ((tp,u):rs) ow = 
      solve (n+1) (compose u s) (tp++gs) ((s,gs,rs):ow)

  backtrack :: Int -> Stack -> [Subst]
  backtrack n []               = []
  backtrack n ((s,gs,rs):ow)   = choose (n-1) s gs rs ow

data Node  = Nd Index [Term] [Term] [Form] deriving Show

type Tableau = [Node]

alpha :: Form -> Bool
alpha (Conj _)       = True
alpha (Neg (Disj _)) = True
alpha _              = False 

beta :: Form -> Bool
beta (Disj _)       = True
beta (Neg (Conj _)) = True
beta _              = False

gamma :: Form -> Bool
gamma (Forall _ _)       = True
gamma (Neg (Exists _ _)) = True
gamma _                  = False

plit, nlit, dneg :: Form -> Bool
plit (Atom n ts)       = True 
plit _                 = False
nlit (Neg (Atom n ts)) = True 
nlit _                 = False 
dneg (Neg (Neg f))     = True
dneg _                 = False 

f2t :: Form -> Term
f2t (Atom n ts)       = Struct n ts
f2t (Neg (Atom n ts)) = Struct n ts

components :: Form -> [Form]
components (Conj fs)          = fs
components (Disj fs)          = fs 
components (Neg (Conj fs))    = map (\ f -> Neg f) fs
components (Neg (Disj fs))    = map (\ f -> Neg f) fs
components (Neg (Neg f))      = [f]
components (Forall x f)       = [f]
components (Neg (Exists x f)) = [Neg f]

binder :: Form -> Id 
binder (Forall x f)       = x 
binder (Neg (Exists x f)) = x 

decompose :: Form -> ([Id],Form)
decompose form = decomp [] form where 
  decomp xs f = if gamma f then decomp (xs ++ [x]) f' else (xs,f) 
      where x    = binder f
            [f'] = components f

step :: Node  -> Tableau 
step (Nd i pos neg []) = [Nd i pos neg []]
step (Nd i pos neg (f:fs)) 
  | plit  f = if elem (f2t f) neg 
              then [] else [Nd i ((f2t f):pos) neg fs]
  | nlit  f = if elem (f2t f) pos
              then [] else [Nd i pos ((f2t f):neg) fs]
  | dneg  f = [Nd i pos neg ((components f) ++ fs)]
  | alpha f = [Nd i pos neg ((components f) ++ fs)]
  | beta  f = [(Nd (i++[n]) pos neg (f':fs)) |
                          (f',n)   <- zip (components f) [0..] ]
  | gamma f = [Nd i pos neg  (f':(fs++[f]))]
    where 
    (xs,g) = decompose f 
    b      = [((Id x j), Var (Id x i)) | (Id x j) <- xs ]
    f'     = appF b g

stepD :: Int -> Node -> (Int,Tableau)
stepD k node@(Nd i pos neg []) = (k,[Nd i pos neg []])
stepD k (Nd i pos neg (f:fs))
  | plit  f = if elem (f2t f) neg 
              then (k,[]) else (k,[Nd i ((f2t f):pos) neg fs])
  | nlit  f = if elem (f2t f) pos 
              then (k,[]) else (k,[Nd i pos ((f2t f):neg) fs])
  | dneg  f = (k,[Nd i pos neg ((components f) ++ fs)])
  | alpha f = (k,[Nd i pos neg ((components f) ++ fs)])
  | beta  f = (k,[(Nd (i++[n]) pos neg (f':fs)) |
                          (f',n)   <- zip (components f) [0..] ])
  | gamma f = (k-1,[Nd i pos neg  (f':(fs++[f]))])
    where 
    (xs,g) = decompose f 
    b      = [((Id x j), Var (Id x i)) | (Id x j) <- xs ]
    f'     = appF b g

expanded :: Node -> Bool 
expanded (Nd i pos neg []) = True
expanded  _                = False

expand :: Int -> Tableau -> Tableau 
expand 0 tableau = tableau 
expand _ []      = []
expand n (node:nodes) = if expanded node 
                       then (node:(expand n nodes))
                       else if k == n 
                       then expand n     (newnodes ++ nodes)
                       else expand (n-1) (nodes ++ newnodes) 
    where (k,newnodes) = stepD n node

checkN :: Node -> [Subst]
checkN (Nd _ pos neg _) = 
   concat [ unifyTs p n | p <- pos, n <- neg ]

appNd :: Subst -> Node -> Node 
appNd b (Nd i pos neg forms) = 
  Nd i (appTs b pos) (appTs b neg) (appFs b forms)

appTab :: Subst -> Tableau -> Tableau
appTab = map . appNd

checkT :: Tableau -> [Subst]
checkT []           = [epsilon]
checkT [node]       = checkN node
checkT (node:nodes) = 
  concat [ checkT (appTab s nodes) | s <- checkN node ]

initTab :: Form -> Tableau 
initTab form = [Nd [] [] [] [form]]

refuteDepth :: Int -> Form -> Bool
refuteDepth k form = checkT tableau /= []
   where tableau = expand k (initTab form)

thm :: Int -> Form -> Bool
thm n = (refuteDepth n) . sk . Neg

sat :: Int -> Form -> Bool
sat n = not . (refuteDepth n) . sk

formula = Disj [Neg trans, Neg symm, Neg serial, refl]

